package no.uio.ifi.cop.cl;

import java.util.ArrayList;
import java.util.Set;
import no.uio.ifi.cop.common.Log;

/**
 * An RHS represents a right hand side of an implication.
 *
 * Since a RHS can represent Conjunctions and Disjunctions
 * its name is a bit generic. To find out what kind of RHS
 * we are dealing with, you can ask for its type (getType).
 *
 * @version 1.0
 * @author bjarneh@ifi.uio.no
 */


public class RHS extends Formula{

    private int cur; // current Conjunction
    private ArrayList<Conjunction> elements;

    public RHS(){
        super();
        cur = 0;
        elements = new ArrayList<Conjunction>(12);
        elements.add( new Conjunction() );
    }

    public void classify(){
        if( elements.size() > 1 ){
            this.type = DISJUNCTION;
        }else{ // size() == 1
            Conjunction first = elements.get(0);
            if( first.getType() == Formula.CONSTANT ){
                this.type = Formula.CONSTANT;
            }else{
                this.type = CONJUNCTION;
            }
        }
    }

    public RHS clone(){

        RHS copy = new RHS();
        Conjunction tmp;

        int max = length() - 1;
        for( int i = 0; i < max; i++){
            tmp = elements.get( i );
            for( Term t : tmp ){
                copy.add( t.clone() );
            }
            copy.disjunct();
        }
        
        for( Term t : elements.get( max ) ){
            copy.add( t.clone() );
        }

        return copy;
    }


    public void add(Term t){
        elements.get(cur).add(t);
    }

    public boolean disjunct(){// ';' has been read
        cur++;
        elements.add( new Conjunction() );
        return true;
    }

    public void gatherVariables(Set<String> set){
        for( Conjunction conj: elements ){
            conj.gatherVariables( set );
        }
    }

    public Conjunction iterFacts(){
        if( length() != 1 ){
            Log.fatal("length() is %d, iterFacts() only works if length() == 1");
        }
        return elements.get(0);
    }

    public Iterable<Conjunction> iterConjunction(){
        return elements;
    }

    public int length(){
        return elements.size();
    }

    public Conjunction get(int i){
        return elements.get( i );
    }

    public String toString(){
        StringBuilder sb = new StringBuilder();
        int max = elements.size() - 1;
        for(int i = 0; i < max; i++){
            sb.append( elements.get(i).toString() ).append("; ");
        }
        sb.append(elements.get(max).toString());
        return sb.toString();
    }

    public RHS apply(Substitution subst){
        for( Conjunction conj : elements ){
            conj.apply( subst );
        }
        return this;
    }
}
